strict_part(x,y.R(x;y);a;b) == R(a;b) & (R(b;a)) 

latex

Up	rel 1, rel 1
Wellformedness Lemmas	strict part wf, strict part wf
Definitions	P & Q, A
FDL editor aliases	strict_part